<html>
<head><meta charset="utf-8"><title>Semantics of functional rust · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html">Semantics of functional rust</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="230162132"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230162132" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230162132">(Mar 13 2021 at 13:13)</a>:</h4>
<p>This is believe to be correct for OCaml. I'm not whether there is a formal proof for this. It has been done for Isabelle by targeting CakeML. See the discussion in sec 5 <a href="https://hal.archives-ouvertes.fr/hal-02380196v2/document">here</a>.<br>
There an discussion <a href="https://github.com/MetaCoq/metacoq/issues/163">issue</a> about the ocaml semantics.<br>
The Galinette teams wants to use semantic typing from Rustbelt for ocaml verification <span class="user-mention" data-user-id="120791">@RalfJ</span> ;-) <br>
<a href="https://coq.discourse.group/t/phd-position-on-certified-extraction-in-nantes/1044">https://coq.discourse.group/t/phd-position-on-certified-extraction-in-nantes/1044</a></p>



<a name="230163921"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230163921" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230163921">(Mar 13 2021 at 13:49)</a>:</h4>
<blockquote>
<p>The Galinette teams wants to use semantic typing from Rustbelt for ocaml verification @RalfJ ;-)<br>
<a href="https://coq.discourse.group/t/phd-position-on-certified-extraction-in-nantes/1044">https://coq.discourse.group/t/phd-position-on-certified-extraction-in-nantes/1044</a></p>
</blockquote>
<p>Awesome. :-)</p>



<a name="230163986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230163986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230163986">(Mar 13 2021 at 13:50)</a>:</h4>
<p><span class="user-mention" data-user-id="382207">@Bas Spitters</span>  regarding the functional fragment of Rust, as a first step I am not even asking for a proof, I am asking for a formal statement of the desired property ;)</p>



<a name="230164807"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230164807" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230164807">(Mar 13 2021 at 14:05)</a>:</h4>
<p>We print from metacoq to rust0 with a restricted form of references and closures.<br>
<a href="https://github.com/AU-COBRA/ConCert/blob/master/extraction/theories/RustExtract.v">https://github.com/AU-COBRA/ConCert/blob/master/extraction/theories/RustExtract.v</a><br>
Let's start easy. Suppose I have a function computing a bool in Coq. Can we prove using rustbelt that this translation computes the same boolean?</p>



<a name="230165480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230165480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230165480">(Mar 13 2021 at 14:17)</a>:</h4>
<p>in terms of langauge semantics, RustBelt is not doing anything clever, or at least not a lot. it is basically a reduced ML-style lambda-calculus (reduced because there are no compound values such as products or sums) with a CompCert-style memory model (products and sums are realized in-memory, like in Rust); the only cleverness is in the concurrency aspect of the memory model where we made sure that data races are UB (so our safety theorem proves absence of data races).</p>



<a name="230165730"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230165730" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230165730">(Mar 13 2021 at 14:21)</a>:</h4>
<p>so doing a proof such as what you are asking for should be basically a standard compiler correctness proof from a purely functional to an imperative language? I guess how hard this is depends on how you represent values and in particular closures, and if there is any sharing going on. Do you use <code>Arc</code> or <code>Box</code> for pointer indirections (I assume you have ptr indirections to support recursive types), and do you rely on Rusts closures or do your own form of closure conversion?</p>



<a name="230165737"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230165737" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230165737">(Mar 13 2021 at 14:21)</a>:</h4>
<p>FWIW, RustBelt is intended to work on the MIR level, which is post closure conversion</p>



<a name="230321912"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230321912" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jakob Botsch Nielsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230321912">(Mar 15 2021 at 10:25)</a>:</h4>
<p>Coming in a bit late to this. We use arena allocation with standard references so that sharing is as simple as possible (with <code>Rc</code>/<code>Arc</code> I believe we would have to clone manually, at least before closures). For closures we rely on Rust closures that live on the heap. One problem with that is that Rust does not support recursive closures, so for internal fixpoints we do recursion through the heap. For an example, this is how we extract the standard <code>ack</code> with its dependencies: <a href="https://gist.github.com/jakobbotsch/39adc8ad1b7ec8d79e240ba098ab7ca9">https://gist.github.com/jakobbotsch/39adc8ad1b7ec8d79e240ba098ab7ca9</a></p>



<a name="230341831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230341831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230341831">(Mar 15 2021 at 13:17)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span>  How much would one obtain by using rustbelt? We are targeting rust and not MIR, moreover rustbelt is not MIR. <br>
In any case, we'll likely wait for the ocaml project to progress, as we can likely profit from that technology.</p>



<a name="230545401"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230545401" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230545401">(Mar 16 2021 at 16:26)</a>:</h4>
<p><span class="user-mention" data-user-id="397574">@Jakob Botsch Nielsen</span> ah so you basically "leak" memory until the end of the computation when the arena is freed? okay yes that makes things easier</p>



<a name="230545848"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230545848" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230545848">(Mar 16 2021 at 16:29)</a>:</h4>
<p><span class="user-mention" data-user-id="382207">@Bas Spitters</span> if you are using only safe code and targeting surface Rust, then RustBelt in its current state is probably not going to help much</p>



<a name="230556957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Semantics%20of%20functional%20rust/near/230556957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jakob Botsch Nielsen <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Semantics.20of.20functional.20rust.html#230556957">(Mar 16 2021 at 17:31)</a>:</h4>
<p>Yep indeed</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>